$\forall$${\it \%xm}$:XM, $T$:Type, $P$:($T$$\rightarrow\mathbb{P}$). ($\exists$$a$:$T$. $P$($a$)) $\Rightarrow$ $P$($\in$$x$:$T$. $P$($x$))